$\forall$$i$:Id, $l$:IdLnk, ${\it tg}$, $n$, $f$, $k$:Top.
\\[0ex]msg{-}spec{-}loc($k$ sends on $l$ with tag ${\it tg}$ [$s$,$v$.$f$($s$,$v$)], at marker $n$;$i$) $\Leftarrow\!\Rightarrow$ (source($l$) = $i$)